perm filename SET.A[1,JRA] blob sn#016815 filedate 1972-12-07 generic text, type T, neo UTF8
00100	PRE_OP:A,B,U,f,SB;
00200	INF_OP:∩;
00300	INF_PRED:ε,≡,⊂;
00400	VAR: x,y,z,u,v,X,Y,Z,V;
00500	a1:((f(x,y)εx ⊃ f(x,y)εy)∧(f(x,y)εy ⊃ f(x,y)εx))⊃x≡y;
00600	a2:x≡y ⊃((zεx ⊃ zεy)∧(zεy ⊃ zεx));
00700	a3:(zεx ∧ zεy) ↔zεx∩y;
00900	a5:(z⊂x ∧ z⊂y)↔ z⊂x∩y;
01000	a7:(z⊂x∧zεU) ↔zεSB(x);
01100	THEOREM: SB(A)∩SB(B) ≡ SB(A∩B);
01200	;
01300	e